i, j:, X:({i..j}). i  x < j. X(x)   

latex

Definitions	i  j < k, x. t(x), x(s), {i..j}, x f y, i  j , T, ff, P  Q, P & Q, P  Q, tt, if b then t else f fi , False, A, A  B, True, , Y, t.2, t.1, 0, +r, e, *, (op,id) lb  i < ub. E(i), r+gp,  lb  i < ub. E(i), <+*>, (r) i  k < j. E(k), a  j < b. E(j), t  T, P  Q, x:A. B(x), P  Q, Dec(P), Unit, , ,
Lemmas	decidable lt, qadd-add, decidable int equal, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, assert of lt int, eqtt to assert, iff transitivity, ge wf, nat properties, bnot wf, le int wf, assert wf, bool wf, lt int wf, le wf, int seg wf, nat wf